Minimal STL parser #4657

MatWise · 2019-05-15T19:01:56Z

Create a basic Siemens STL parser and integrate it into CBMC.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

tautschnig · 2019-05-16T07:06:18Z

This looks really nice and clean overall - my only concern is the ambiguity of the acronym "STL." It just seems too easy to confuse with "Standard Template Library," especially when the framework also (partly) supports analysis of C++ code. Is there any chance to choose a different name?

src/structured-text/converters/convert_int_value.cpp

src/structured-text/structured_text_parser.cpp

src/structured-text/structured_text_parser.h

src/structured-text/structured_text_typecheck.cpp

src/structured-text/converters/convert_int_value.cpp

src/structured-text/structured_text_language.cpp

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 138102e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/113086645
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

unit/CMakeLists.txt

unit/Makefile

allredj · 2019-05-24T14:28:08Z

This compiles with TG fine. You can disregard the bot message (@MatWise is a "first time contributor" and TG CI does not fetch his fork). ✔️

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: f4cf421).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/113109006
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

src/structured-text/converters/convert_bool_literal.cpp

src/structured-text/converters/convert_int_literal.cpp

tautschnig

This is overall very nicely done!!! Just one request in addition to all the nit-picks below: could you please make sure that all "TODO" comments include sufficient information for someone else to pick this up and work on it?

src/structured-text/CMakeLists.txt

src/structured-text/converters/convert_int_literal.h

src/structured-text/converters/convert_string_value.h

src/structured-text/converters/expr2structured_text.cpp

src/structured-text/parser.y

src/structured-text/scanner.l

src/structured-text/structured_text_language.cpp

src/structured-text/structured_text_language.h

src/structured-text/structured_text_parser.cpp

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: f3b4b65).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/113740279
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: eb31831).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/113772968
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: d484911).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/113899257
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: d666742).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/113901720
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

Includes support for simple arithmetic and boolean expressions as well as other Statement List language features, such as networks, functions and function blocks.

Includes a basic Statement List language interface (although without any typechecking yet) as well as modifications to some Makefiles and cbmc_languages.cpp. Use the --show-parse-tree option when parsing a .awl file to see the project's output.

Includes tests for simple integer additions/multiplications, multiple functions/function blocks and for dividing two floats.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 2ba1361).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/113911945
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

codecov-io · 2019-05-31T16:30:36Z

Codecov Report

❗ No coverage uploaded for pull request base (develop@3f9e1b0). Click here to learn what that means.
The diff coverage is 61.66%.

@@            Coverage Diff             @@
##             develop    #4657   +/-   ##
==========================================
  Coverage           ?   68.42%           
==========================================
  Files              ?     1269           
  Lines              ?   104649           
  Branches           ?        0           
==========================================
  Hits               ?    71606           
  Misses             ?    33043           
  Partials           ?        0

Impacted Files	Coverage Δ
.../statement-list/converters/expr2statement_list.cpp	`0% <0%> (ø)`
src/statement-list/statement_list_typecheck.cpp	`0% <0%> (ø)`
src/statement-list/statement_list_typecheck.h	`0% <0%> (ø)`
...statement-list/converters/convert_bool_literal.cpp	`0% <0%> (ø)`
src/cbmc/cbmc_languages.cpp	`100% <100%> (ø)`
...statement-list/converters/convert_real_literal.cpp	`100% <100%> (ø)`
.../statement-list/converters/convert_int_literal.cpp	`33.33% <33.33%> (ø)`
src/statement-list/statement_list_language.cpp	`42.85% <42.85%> (ø)`
src/statement-list/scanner.l	`57.69% <56.86%> (ø)`
src/statement-list/parser.y	`58.78% <58.78%> (ø)`
... and 5 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 3f9e1b0...2ba1361. Read the comment docs.

MatWise requested review from chrisr-diffblue, kroening, peterschrammel, smowton and tautschnig as code owners May 15, 2019 19:01

MatWise force-pushed the feature/minimal-stl-parser branch 5 times, most recently from f76926a to 96157f2 Compare May 20, 2019 17:05

pkesseli suggested changes May 20, 2019

View reviewed changes

MatWise force-pushed the feature/minimal-stl-parser branch from 96157f2 to 58c2a56 Compare May 21, 2019 20:26

romainbrenguier reviewed May 22, 2019

View reviewed changes

pkesseli approved these changes May 22, 2019

View reviewed changes

MatWise force-pushed the feature/minimal-stl-parser branch 5 times, most recently from 7c3ae4d to 138102e Compare May 24, 2019 11:53

allredj reviewed May 24, 2019

View reviewed changes

unit/CMakeLists.txt Outdated Show resolved Hide resolved

allredj reviewed May 24, 2019

View reviewed changes

unit/Makefile Outdated Show resolved Hide resolved

MatWise force-pushed the feature/minimal-stl-parser branch from 138102e to f4cf421 Compare May 24, 2019 14:35

allredj reviewed May 24, 2019

View reviewed changes

pkesseli suggested changes May 28, 2019

View reviewed changes

tautschnig approved these changes May 28, 2019

View reviewed changes

MatWise force-pushed the feature/minimal-stl-parser branch 2 times, most recently from 41c2762 to f3b4b65 Compare May 30, 2019 09:48

MatWise force-pushed the feature/minimal-stl-parser branch from f3b4b65 to eb31831 Compare May 30, 2019 14:46

allredj reviewed May 30, 2019

View reviewed changes

MatWise force-pushed the feature/minimal-stl-parser branch 2 times, most recently from d484911 to d666742 Compare May 31, 2019 13:53

allredj reviewed May 31, 2019

View reviewed changes

pkesseli approved these changes May 31, 2019

View reviewed changes

MatWise added 3 commits May 31, 2019 16:40

Add basic Statement List parser

37f60f2

Includes support for simple arithmetic and boolean expressions as well as other Statement List language features, such as networks, functions and function blocks.

Integrate STL parser into CBMC executable

b900edc

Includes a basic Statement List language interface (although without any typechecking yet) as well as modifications to some Makefiles and cbmc_languages.cpp. Use the --show-parse-tree option when parsing a .awl file to see the project's output.

Add Statement List regression tests

2ba1361

Includes tests for simple integer additions/multiplications, multiple functions/function blocks and for dividing two floats.

MatWise force-pushed the feature/minimal-stl-parser branch from d666742 to 2ba1361 Compare May 31, 2019 15:40

allredj reviewed May 31, 2019

View reviewed changes

pkesseli merged commit 6c39035 into diffblue:develop May 31, 2019

Minimal STL parser #4657

Minimal STL parser #4657

Uh oh!

Conversation

MatWise commented May 15, 2019

Uh oh!

tautschnig commented May 16, 2019

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

allredj commented May 24, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

codecov-io commented May 31, 2019

Codecov Report

Uh oh!

Uh oh!